CBC Casper: Finality inspector (Japanese)
Prerequisites
Safety oracle
Whitepaperのsection 7: Clique oracleの証明(未完成)
Inspectorとは
Safety oracleの一種、割と新しいアイデア (元記事) 数学者が考えた
※たくさんlayer(上の記事ではlevel)を重ねるようなことが提案されてるけど、とりあえず1-layerがターゲット(重ねる意味はないと思っている)
Finalityを検知する(true/falseを返す)関数自体をInspectorと呼ぶ
が、今の所、Inspectorがtrueを返すようなMessage DAGの状態のこともInspectorと呼んでる（もっとグラフっぽい名前にしたい）
例: "Inspector preserved over immediately next message"
https://gyazo.com/df05b8a007ef386f36fbbe434e713efd
Why "no later disagreeing"?
$ \sigmaでのLatest messageと$ \mathrm{L^H_J(\sigma)(v)}でのLatest messageの間に別のmessageが存在するかもしれない
https://gyazo.com/5169be8bfae11d27967e89eb9562a78b
Inspectorの正しさの証明
ゴール: Lemma 40
"あるproperty pに対するInspectorがあると、(equivocationがt以下である限り)全てのfuture stateでpが成り立つ"
基本的には、WhitepaperのSection7 (Clique oracleの証明、ただしところどころ未完成)がベース
Section7は7.1~7.5の5つのsubsectionに分かれていて、各章の一番最後のlemmaがゴールで、それ以外lemmaはそのゴールを示すためのもの
変更点
Clique OracleじゃなくてInspectorになってる
Minimal transitionじゃなくてimmediately next message
証明の進め方
元の証明は、state transition, message justificationの補題が少ないまま進めているので、多分無駄が多い(はず)
ので、sorryを多用して後ろからせめて、どんどん無駄な補題を削っていけばいいのでは？
証明の大枠
Lemma 38: Inspectorがあると、そのpropertyは成りたつ
DONE! lemma (in Protocol) inspector_imps_estimator_agreeing
Lemma 39: あるstateにおいてInspectorが存在すると、(equivocationがt以下である限り)任意のfuture stateにおいてinspectorが存在
Lemma 36: Inspectorはimmediately next messageを受け取った次のstateでも存在
方針: Immediately next messageが何かで場合分け
Lemma 33: SenderがInspectorのメンバーではない
Done! inspector_preserved_over_message_from_non_member
Lemma 34: SenderがInspectorのメンバーで、equivocationしてない
Lemma 35: SenderがInspectorのメンバーで、equivocationしてる
Lemma 39をLemma36から帰納的に証明
"任意のfuture stateは、immediately next messageによる状態遷移を繰り返すことで到達する"
任意のfuture stateの間にimmediately_next_messageが存在することは示してある
https://gyazo.com/c3e3769029d3f7cffb1233db50b682b5